\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$, $B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$), $m$:$\mathbb{N}$,\+
\\[0ex]$L$:event{-}info(${\it ds}$;${\it da}$) List, $z$:event{-}info(${\it ds}$;${\it da}$).
\-\\[0ex]let ${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$ = $A$ in 
\\[0ex]let ${\it Tb}$,${\it ksb}$,${\it ib}$,${\it gb}$,${\it hb}$,${\it ab}$,${\it eb}$ = $B$ in 
\\[0ex]${\it Ta}$ $=$ ${\it Tb}$ $\in$ Type
\\[0ex]\& ${\it ksa}$ $=$ ${\it ksb}$ $\in$ Knd List \& ${\it ia}$ $=$ ${\it ib}$ $\in$ ${\it Ta}$
\\[0ex]\& \=${\it aa}$ $=$ ${\it ab}$ $\in$ $\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ksa}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it Ta}$$\rightarrow\mathbb{B}$)\+
\\[0ex]\& (\=$\forall$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List, $k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ksa}$) \}, $s$:State(${\it ds}$), $v$:Valtype(${\it da}$;$k$).\+
\\[0ex]${\it L'}$ @ [$\langle$$k$$,\,$$s$$,\,$$v$$\rangle$] $\leq$ $L$
\\[0ex]$\Rightarrow$ ${\it gb}$($k$,$s$,$v$,ecl{-}trans{-}state($A$;${\it L'}$)) $=$ ${\it ga}$($k$,$s$,$v$,ecl{-}trans{-}state($A$;${\it L'}$)) $\in$ ${\it Ta}$)
\-\-\\[0ex]$\Rightarrow$ ecl{-}trans{-}act(${\it ds}$;${\it da}$;$A$)($m$,$L$ @ [$z$])
\\[0ex]$\Rightarrow$ ecl{-}trans{-}act(${\it ds}$;${\it da}$;$B$)($m$,$L$ @ [$z$])
\end{tabbing}